% Capitoulul 1 - 6 pag

\chapter{Motiva\c tie} % Titlul capotilului
\label{Capitolul1}

\section{Verificarea programelor}

Odat\u a cu cre\c sterea complexit\u a\c tii proiectelor software, verificarea calit\u a\c tii programelor a devenit o problem\u a principal\u a a ingineriei software. Aceast\u a verificare este necesar\u a \^ in mai multe contexte. Odat\u a cu dezvoltarea platformelor de agen\c ti mobili, a ap\u arut nevoia de verificare a codului de la distan\c t\u a care urmeaz\u a s\u a fie executat de c\u atre un sistem gazd\u a. O alt\u a utilizare a metodelor de verificare a programelor este \^ in verificarea conformit\u a\c tii programelor cu o specifica\c tie dat\u a. De aseamenea, compilatoarele trebuie s\u a efectueze o serie de verific\u ari pentru a confirma legitimitatea aplic\u arii unor optimiz\u ari cu p\u astrarea semanticii programului ini\c tial. De exemplu, dac\u a se poate verifica faptul c\u a ambii termeni ai unei adun\u ari au valori constante, cunoscute la compilare, atunci rezultatul ei poate fi calculat, la r\^ andul sau, la momentul compil\u arii.

\section[Problema verific\u arii statice]{Problema verific\u arii statice a programelor}

De\c si in aplica\c tii practice este folosit\u a preponderent verificarea dinamic\u a a programelor sub forma test\u arii, aceast\u a abordare folose\c ste doar pentru demonstra\c tii negative ale unor propriet\u a\c ti. Din aceast\u a cauz\u a, solu\c tia ideal\u a pentru toate problemele enun\c tate in paragraful anterior ar fi existen\c ta unui instrument software care s\u a verifice static, doar pe baza codului surs\u a, anumite propriet\u ati ale programelor.

\subsection[Teorema lui Rice]{Teorema de nedecidabilitate a lui Rice}

Este un fapt \c stiut c\u a solu\c tia indicat\u a \^ in pragraful anterior este imposibil\u a.

\begin{theorem}[Rice]
Orice proprietate extensional\u a \c si netrivial\u a a programelor este nedecidabil\i a.
\end{theorem}

Aceast\u a teorem\u a se bazeaz\u a pe problema opririi ma\c sinilor Turing.

\begin{theorem}[Turing,1936]
Problema opririi unei ma\c sini Turing este nedecidabil\u a.
\end{theorem}

Teorema aceasta st\u a la baza rezultatelor de nedecidabilitate ale multor probleme care apar  \^ in construc\c tia compilatoarelor, de exemplu, \emph{"variabila x poate fi $>$ 0  \^ in punctul P din program"}.

Totu\c si experien\c ta ne arat\u a c\u a majoritatea programelor folosite  \^ i\c si termin\u a execu\c tia , sau prelucreaz\u a un flux de date de intrare \c si prelucrarea fiec\u arui element din fluxul de date de intrare se termin\u a .

\begin{example}
Compilatoarele sau func\c tiile de criptare sunt programe a c\u aror execu\c tie trebuie s\u a se termine. Alte exemple sunt func\c tiile folosite in implementarea unor structuri de date. Din a doua clas\u a, fac parte programele cu interfa\c ta grafic\u a \c si sistemele de operare. Prelucrarea fiec\u arei cereri din partea utilizatorului se termin\u a de fiecare dat\u a.
\end{example}

\subsection{Solu\c tii}

De\c si nedecidabil\u a, problema verific\u arii statice are mai multe solu\c tii par\c tiale.

Un exemplu de astfel de solu\c tie este aceea  \^ in care demonstra\c tia este generat\u a de un instrument software (theorem prover) care are la baz\u a o logic\u a cu o expresivitate ridicat\u a \c si care necesit\u a, eventual, interac\c tiune uman\u a. Aceast\u a variant\u a este folosit\u a de cel care produce programul pentru a demonstra anumite propriet\u a\c ti ale acestuia.  \^ In contextul dezvolt\u arii bazate pe componente, aceast\u a demonstra\c tie trebuie facut\u a o singur\u a dat\u a \c si apoi programul poate fi refolosit f\u ar\u a a reface demonstra\c tia. Un exemplu de astfel de instrument este Isabelle bazat pe logica de ordin  \^ inalt.

O alta variant\u a este cea folosit\u a  \^ in compilatoare pentru a decide propriet\u a\c tile necesare pentru a asigura corectitudinea optimiz\u arilor  \^ in ceea ce prive\u ste semantica limbajului de programare. Aceast\u a solu\c tie folose\c ste o procedur\u a de decizie corect\u a, dar incomplet\u a care poate decide doar anumite tipuri de propriet\u a\c ti \citep{1095594}. Aceast\u a solu\c tie se bazeaz\u a pe algoritmul Kildall \c si are meritul c\u a este rapid\u a \c si este complet automat\u a.

\^ In concluzie trebuie f\u acut un compromis  \^ intre expresivitatea metodei de demonstra\c tie pe de o parte \c si complexitatea algoritmului de generare a demonstra\c tiilor \c si a sistemului logic pe care se bazeaz\u a \c si necesitatea interven\c tiei umane pe de alt\u a parte.

\section{Theorem prover}

O abordare care folose\c ste theorem prover este cea numit\u a Proof-carrying code \citep{ATTAPL}.  \^ In aceast caz cel care scrie codul este responsabil s\u a furnizeze \c si o demonstra\c tie asupra functionalit\u a\c tii codului  \^ in conformitate cu specifica\c tia. Pentru aceast\u a sarcin\u a sunt folosite mai multe elemente:

\begin{itemize*}
  \item un \textbf{limbaj de specificare formal\u a} cu ajutorul c\u aruia se exprim\u a proprietatea de func\-\c ti\-o\-na\-re sigur\u a a programului
  \item o \textbf{logic\u a} pentru a face legatura intre \textbf{specificatie} si \textbf{semantica limbajului} de programare folosit. Se poate folosi, spre exemplu, logica Hoare \citep{363259}.
  \item un \textbf{limbaj pentru scrierea demonstra\c tiei}
  \item un \textbf{algoritm de validare a demonstra\c tiilor},  \^ in general asociat cu limbajul in care se exprima demonstratia.
  \item \textbf{instrumente pentru generarea automat\u a a demonstra\c tiilor (theorem provers)}, dar p\u ar\c tile mai complicate din demonstra\c tie pot fi f\u acute \c si manual.
\end{itemize*}
\done\todo{citez PCC}

Nevoia interac\c tiunii umane nu provine din considerente de expresivitate, ci de complexitate a algoritmului de generare a demonstra\c tiei. Ca principiu, interac\c tiunea uman\u a ar putea fi  \^ inlocuit\u a de o component\u a de nedeterminism a algoritmului. Acesta poate pur  \c si simplu \emph{s\u a ghiceasc\u a} deciziile luate de partea uman\u a. Concluzia c\u a interac\c tiunea uman\u a nu este necesar\u a din punctul de vederee al expresivit\u a\c tii este dat\u a de urmatoarea teorem\u a.

\begin{theorem}
Clasa de limbaje recunoscute de ma\c sini Turing deterministe coincide cu clasa de limbaje recunoscute de ma\c sini Turing nedeterministe.
\end{theorem}

Totu\c si, din punct de vedere al complexit\u a\c tii se crede c\u a ma\c sinile Turing nedeterministe sunt mai puternice dec \^ at cele deterministe,  \^ in sensul c\u a, pot rezolva o clas\u a mai bogat\u a de probleme  \^ in timp polinomial ( celebra problem\u a \emph{P = NP} ).

\subsection{Arhitectura}

\done\todo{comentat poza}
Dup\u a cum se vede din imaginea care prezint\u a un sistem de verificare ce folose\c ste un theorem prover, interac\c tiunea uman\u a este necesar\u a  \^ in mai multe etape ale procesului de demonstra\c tie. Pe lang\u a ac\c tiunea fireasc\u a de scriere de cod folosind un limbaj de programare, programatorul trebuie sa foloseasc\u a \c si un limbaj de specificare  \^ in care s\u a exprime proprietatea dorit\u a \c si un limbaj de scriere a demonstra\c tiei,  \^ in care s\u a completeze p\u ar\c tile mai complicate ale demonstra\c tiei f\u acute automat de c\u atre generatorul de demonstra\c tii.

\^ In general, limbajele de demonstra\c tie au o semantic\u a mult mai complex\u a dec\^ at limbajele de programare \c si sunt bazate pe fundamente logice matematice.

\begin{center}
    \input{Imagini/thm_prover_arch.tex}
%    \includegraphics[width=350pt]{thm_prover_arch.png}\\
    \label{thm_prover_arch}
\end{center}

\subsection{Conjectura Collatz}

Un dezavantaj al abord\u arii  \^ in care demonstra\c tiile includ p\u ar\c ti ce trebuie f\u acute de c\u atre programatori este c\u a exist\u a propriet\u a\c ti simple a caror demonstra\c tie se dovede\c ste suficient de complicat\u a. Astfel, programatorii sunt pu\c si  \^ in situa\c tia nefireasc\u a de a stabili dac\u a o proprietate este nedecidabil\u a, sau dac\u a merit\u a investit efort  \^ in demonstra\c tia ei. Un exemplu de astfel de demonstra\c tie care pare simpl\u a este \emph{problema 3n+1}:
\begin{quote}
    Plec\^ and de la un numar $n$ , daca el este par atunci \^il \^imp\u ar\c tim la 2, altfel \^il \^inmultim cu 3 si adun\u am 1. Apoi continu\u am procedeul cu num\u arul ob\c tinut. Este adev\u arat c\u a pornind de la orice numar, ajungem \^in final la 1?
\end{quote}

Aceast\u a problem\u a este echivalent\u a cu terminarea urmatorului program:

\begin{lstlisting}
--- Conjectura Collatz
let collatz |<Nat->Nat>| :=
    letrec |<Nat->Nat>| collatz_ :=
        fn |<Nat->Nat>| n =>
            (if|<Nat>|
                (eqNat n one)
                one
                (if|<Nat>|
                    (eqNat(mod n two) z)
                    (collatz_ (div n two))
                    (collatz_ (add (mul n three) one))
                )
            )
\end{lstlisting}

De\c si pare c\u a raspunsul este \emph{da} \c si propozi\c tia a fost verificat\u a pan\u a la numere foarte mari cu ajutorul calculatorului, problema este \^in stadiul de conjectur\u a din anul 1937. Alte probelme de acela\c si gen sunt teorema Fermat, conjectura Goldbach, etc.


\section{Demonstrarea automat\u a a termin\u arii}

O solu\c tie fezabil\u a pentru problema verific\u arii statice este una \^in care programatorii scriu cod folosind un limbaj de programare, iar propriet\u a\c tile dorite sunt demostrate \^in mod automat de c\u atre unele instrumente software, de exemplu de c\u atre compilator. \^In cele ce urmeaz\u a voi trata \^in principal proprietatea de terminare.

\subsection{Arhitectura}
\done\todo{comentat poza}

Arhitectura unui sistem de automat de verificare este mult mai simpl\u a. Singura ac\c tiune \^in care este implicat\u a partea uman\u a este cea de scriere de cod. Problema principal\u a cu aceast\u a arhitectur\u a este lipsa de flexibilitate, propriet\u a\c tile care se pot verifica fiind integrate \^in compilator. Totu\c si o proprietate de genul \emph{programul \^intoarce mereu rezultatul \textbf{TRUE}}, poate fi folosit\u a pentru a exprima echivalen\c ta a doua programe sau unii invarian\c ti.

\begin{center}
    \input{Imagini/tbt_arch.tex}
%    \includegraphics[width=350pt,height=100pt]{tbt_arch.png}\\
    \label{tbt_arch}
\end{center}


\subsection{Abord\u ari existente}

O prim\u a simplificare a problemei este reprezentat\u a de \^inlaturarea buclelor de control din limbajul de programare. Astfel singura posibilitate de a avea o expresie a c\u arei evaluare nu se termin\u a este dat\u a de prezen\c ta func\c tiilor textual recursive. Dac\u a impunem asupra acestora restic\c tia ca fiecare apel al unei func\c tii recursive s\u a fie facut asupra unor parametri \emph{mai mici}, atunci stiva de apeluri succesive va fi un sir de descrescator de parametri. Pentru a demonstra finitudinea stivei de apeluri recursive, este suficient s\u a ar\u atam c\u a rela\c tia de \emph{mai mic} este \fixme{well-founded}.

\begin{definition}\label{well_founded}
O rela\c tie de ordine $R$ este \fixme{\textbf{well-founded}} dac\u a nu exist\u a nici un \c sir infinit de elemente $x_1, \dots , x_n, \dots$ astfel \^incat $x_{i+1} R x_i,\forall i$.
\end{definition}

\done\todo{exemplu condi\c tii sintactice}
\begin{example}
Un exemplu de rela\c tie de ordine de natur\u a sintactic\u a \^intre expresii este urmatoarea:
    \begin{itemize*}
      \item Argumetele s\u a apar\c tin\u a unui tip de pentru care relatia de subtermen este \fixme{well-founded} (de exemplu tip de date algebric).
      \item Apelurile recursive ale func\c tiei sunt f\u acute doar asupra unor subtermeni ai argumentelor. Ace\c sti subtermeni sunt ob\c tinuti prin deconstruc\c tia argumentelor, folosind de exemplu analiza de cazuri sau pattern matching (\^in limbajul Haskell).
    \end{itemize*}
\end{example}

\done\todo{dezavantaje condi\c tii sintactice, din 5}
Un dezavantaj \^in folosirea condi\c tiilor de natur\u a sintactic\u a este c\u a acestea sunt foarte sensibile la modul \^in care este scris programul.

\begin{example}
De exemplu programul \ref{syntactic_ok} respect\u a condi\c tia de mai sus, \^in timp ce programul \ref{syntactic_bad}, de\c si echivalent din punct de vedere func\c tional, nu o respect\u a.
\end{example}
\begin{lstlisting}[label=syntactic_ok,captionpos=b,caption=Exemplu corect,float=tb]
letrec const0 |<Nat->Nat>| :=
fn |<Nat>| n => case n of {
    z => z
    s => fn|<Nat>| pn =>
        (const0 pn)
}
\end{lstlisting}
\begin{lstlisting}[label=syntactic_bad,captionpos=b,caption=Exemplu incorect,float=tb]
letrec const0 |<Nat->Nat>| :=
fn |<Nat>| n => case n of {
    z => z
    s => fn|<Nat>| pn =>
        (const0 ((fn |<Nat>| x => x) pn))
}
\end{lstlisting}
\done\todo{recursori pe structuri de date, catamorfism}

\subsection{Integrarea cu teoria tipurilor}

O solu\c tie natural\u a este aceea de a face demonstra\c tiile \^in faza de compilare a programului. Pasul cel mai potrivit \^in cadrul compil\u arii este cel al analizei de tip, c\^and compilatorul oricum face demonstra\c tii ale faptului c\u a o expresie are un anumit tip. Ideea termin\u arii bazate pe tipuri este aceea de a asocia tipuri doar acelor expresii a c\u aror evaluare se termin\u a.

Avantajul principal al acestei solu\c tii este acela c\u a programatorii nu trebuie s\u a inve\c te noi limbaje de specifica\c tie, \c si sisteme logice de demonstra\c tie. Folosirea unor sisteme de tipuri, fie ele \c si mai exotice, reprezint\u a o sarcin\u a mai u\c soar\u a pentru un programator dec\^at folosirea unor formalisme matematice complexe. Sistemele de tipuri ascund \^in general fundamentele teoretice pe care se bazeaz\u a \t si astfel pot fi folosite si de c\u atre cei care nu le \^in\c teleg.

\^ In ciuda simplit\u a\c tii, aceast\u a metod\u a are dezavantajul c\u a atunci c\^and sistemul de tipuri nu este suficient de puternic pentru a demonstra terminarea evalu\u arii unei expresii, aceasta nu poate fi facut\u a manual. Un alt dezavantaj este c\u a limbajul care folose\c ste acest sistem de tipuri nu este Turing complet. 